Implemented Un (unary) operations for Interval Propagation domain;
Improved ValidSize, ValidStore, Addable, Comparable, TypeConstraint,
LoadMapFd for Interval Prop.;
Added implementation for ValidAccess for Interval Prop.;
Refactored other code;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Fixed printing control that was causing unnecessary analysis to run, and
causing assert fails, when -v option not provided

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Checking that stack is all numeric in certain location was needed in the
Valid Access check;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

The Valid Access was not being checked correctly when width is stored in
a register, hence it passed the cases when it should fail;
For Region and Offset domain, added required implementations;
Refactoring and simplification in Type and Interval Propagation domains;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

In Un, the forgetting of the registers in Offset and Region domain was
added;
In Call, proper forgetting of stack cells in Offset and Region domain
was added;
Removed some redundant code in Type domain;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

In Call and Packet, scratch caller saved registers functionality is
added for all domains;
In Call, for the Offset domain, the packet pointer forgetting is added
(it is already implemented in Region domain but was missing in Offset);

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Previously, the value for dst in Un was being forgotten if certain
conditions did not meet, but that should have just stored a TOP number,
instead of forgetting;
Printing the Un operation;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Implemented ValidDivisor, that was missed;
Refactored/Moved to Type domain from sub-domains the following:
ValidSize, Addable, ValidStore;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Multiple refactorings done in order to simplify operations, remove
redundant operations, and improve readability of the code;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

print option was being passed to all transformers in all domains, since
previously prints were done in respective transformers;
it has been cleaned up;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Temporarily disable all asserts that related to checking if the type of
a register is defined in both region and interval propagation domain;
These should not fail, but for certain benchmarks, these do (needs to be
checked later);
Some refactoring in the code of assert checks;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Added the concept of nullness of a pointer as MAYBE_NULL, NOT_NULL, and
_NULL;
Keeping track of pointer aliases for shared ptrs;
Support for Assume operation for shared ptrs, and null check for shared
ptrs in ValidAccess;
Better join, including join for shared ptr aliases;
Some refactoring, mainly related to join operations;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Needs more work, some test cases might still not be added for type
domain

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Making setup_entry method in type domain, and region domain parametric,
to allow initialization of r1 as ctx ptr based on the scenario;
Some changes also made to crab_verifier, which defines those cases;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

string_invariants are required to run the test cases in the prevail
framework, hence such support is added for type domain;
This includes support for creating the string invariant, and converting
it back to actual types;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Support for running tests for both ebpf domain and type domain inside
the single framework;
Some refactoring in crab_verifier;
Some fixes added in each sub-domain for the tests;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Previously, the interval propagation domain handled the intervals in a
similar manner for both signed and unsigned operations, with some
specific cases handled for unsigned separately, which is unsound;
Currently, signed interval domain handles signed operations, and
unsigned intervals handles unsigned, while the interval domain manages
both using 'reduction';
Some cleanup/refactoring, and better handling of dependencies;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Some cleanup of redundant code and transformers;
Commenting some code related to assertions in the code, since those
assertions are commented for now, activate later;
Simplifying a check related to stack all numeric in ValidMapKeyValue;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Added implementation to represent begin, end, meta, and other slack
variables a_0, a_1, ... for offset domain

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Removing some code that is not currently adding any functionality to
current benchmarks, conservatively;
In future, add more sophisticated analysis;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Added some extra checks to identify potential issues;
Refactoring

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Major change: rather than keeping pointer to values of slacks in each of
these classes, use a single pointer that is being passed to wherever it
is needed;
A lot of cleanup of code, addressed some minor issues;
Better printing;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Packet access required for constraints when not comparing different
packet symbols, which needed special handling;
Renamed some functions for better understanding;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

The code was accidentally removed before, to check for a stack numeric
access when the access type is read, which has been added;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

When loading a numerical value, there should not be an overlap with
packet pointers, which was incorrectly being reported due to bad
computation of offsets; Fixed now

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Removed previously added overflow checks, needs revisiting;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Since these checks make previously verified benchmarks to be unsafe,
special care is needed;
Recheck later;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

These refinements generally do not help with packet operations, so using
slacks with these should not help, hence removed it;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

For joins, pointers should have exact width; even if this doesn't work
in all cases, it gives a safe analysis;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

For now, extra annotations have not been added like stack locations
accessed, and types on the right-hand side;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

For now, all important instructions can print relevant register
information, and each basic block prints initial types;
Call instruction needs to print the types of parameters;
Need to print stack content information as well;

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

This only prints the register types for arguments and return value

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>

Signed-off-by: Ameer Hamza <ah18r@fsu.edu>